Erasure-No-Project-Erased-Match.agda:12,32-33
Variable x is declared erased, so it cannot be used here
when checking that the expression x has type A
